1. Technical Field
The present invention relates to static code analysis and, more particularly, to using multiple analyses with differing levels of precision to make static analysis reports more useful.
2. Description of the Related Art
Static code analysis is a powerful approach for software verification. Static analysis typically features one-sided error: a subject program is safe with regard to the tested property if no violations of the property are discovered by the analysis, which over-approximates the program's set of possible behaviors. However, if the analysis does report violations of the property, then that doesn't necessarily imply that the program is incorrect. These violations may be false reports due to the approximations the analysis applies to put bounds on the state space of the program, which could otherwise be infinite.
Since the tested properties are mostly hard to verify statically (e.g., security vulnerabilities, concurrency bugs, typestate violations, etc.), static analysis tools typically have a high proportion of false reports. For example, commercial static security tools—such as IBM Rational AppScan Source Edition and HP Fortify 360—would report about 10,000 vulnerabilities on a program containing 100,000 LOC. This limits the usability of commercial analysis tools: The size of the report, together with the poor quality of many of the findings, makes it difficult to translate the report into an actionable list of remediation tasks.